package org.barad.architecture.analyzer.model.impl;

import java.util.ArrayList;
import java.util.LinkedList;
import java.util.List;

import kodkod.ast.Formula;
import kodkod.ast.Relation;
import kodkod.engine.Solution;
import kodkod.engine.Solver;
import kodkod.engine.satlab.SATFactory;
import kodkod.instance.Bounds;
import kodkod.instance.TupleFactory;
import kodkod.instance.TupleSet;
import kodkod.instance.Universe;

public class SimpleModel {

	private Bounds bounds;
	private Relation data = Relation.unary("data");
	private Relation connector = Relation.unary("connector");
	private Relation test = Relation.binary("test");
//	private Relation name = Relation.unary("name");
//	private Relation componentName = Relation.binary("componentName");
	
	public void init() {
//		List<String> atoms = new LinkedList<String>();
//		atoms.add("Data");
//		atoms.add("Connector");
//		atoms.add("Name0");
//		atoms.add("Name1");
//		//atoms.add("Connector1");
//		Universe universe = new Universe(atoms);
//		bounds = new Bounds(universe);
//		TupleFactory factory = universe.factory();
//		//data relation
//		TupleSet dataTuples = factory.noneOf(1);
//		dataTuples.add(factory.tuple("Data"));
//		bounds.boundExactly(data, dataTuples);
//		//connector relation
//		TupleSet connectorTuples = factory.noneOf(1);
//		connectorTuples.add(factory.tuple("Connector"));
//		bounds.boundExactly(connector, connectorTuples);
//		//name realtion
//		TupleSet nameTuples = factory.range(factory.tuple("Name0"), factory.tuple("Name1"));
//		//nameTuples.add(factory.tuple("Name1"));
//		bounds.boundExactly(name, nameTuples);
//		//name realtion
//		TupleSet componentNameTuples = factory.noneOf(2);
//		componentNameTuples.add(factory.tuple("Data", "Name1"));
//		componentNameTuples.add(factory.tuple("Connector", "Name1"));
//		bounds.boundExactly(componentName, componentNameTuples);
	
	
		List<String> atoms = new LinkedList<String>();
		atoms.add("Atom");
		atoms.add("Test1");
		Universe universe = new Universe(atoms);
		bounds = new Bounds(universe);
		TupleFactory factory = universe.factory();
		//data
		TupleSet dataSet = factory.noneOf(1);
		dataSet.add(factory.tuple("Atom"));
		bounds.boundExactly(data, dataSet);
		//connector
		TupleSet connectorSet = factory.noneOf(1);
		connectorSet.add(factory.tuple("Atom"));
		bounds.boundExactly(connector, connectorSet);
		//test
		TupleSet testSet = factory.noneOf(2);
		testSet.add(factory.tuple("Atom", "Atom"));
		bounds.boundExactly(test, testSet);
	}
	
	
	public Formula noCommonNames() {
		Formula formula = data.join(test).intersection(connector).one();
		return formula;
	}
	
	public Bounds getBounds() {
		return bounds;
	}
	
	public static void main(String[] args) {
		SimpleModel model = new SimpleModel();
		model.init();
		Solver solver = new Solver();
		solver.options().setSolver(SATFactory.LightSAT4J);
		//all names must be unique
		Solution solution = solver.solve(model.noCommonNames(), model.getBounds());
		System.out.println(solution);
	}
}
